Nuprl Lemma : R-realizes_wf
0,22
postcript
pdf
R
:es_realizer{i:l},
P
:(ES{i}
Prop{i'}).
R
||-{i}
es
.
P
(
es
)
Prop{i''}
latex
Definitions
x
:
A
.
B
(
x
)
,
Prop
,
t
T
,
R
||-
es
.
P
(
es
)
,
x
(
s
)
,
P
&
Q
,
P
Q
Lemmas
R-Feasible
wf
,
event
system
wf
,
R-consistent
wf
,
es
realizer
wf
origin
R:es_realizer{i:l}, P:(ES{i}
Prop{i'}). R ||-{i} es.P(es) 
Prop{i''} R:es_realizer{i:l}, P:(ES{i}Prop{i'}). R ||-{i} es.P(es) Prop{i''} x:A. B(x) T
Q